Nuprl Lemma : div_elim
13,42
postcript
pdf
a
:
,
n
:
.
q
:
. (Div(
a
;
n
;
q
) & (
a
n
) =
q
)
latex
Up
int
2
,
int
2
Definitions
t
T
,
x
:
A
.
B
(
x
)
,
,
P
&
Q
,
x
:
A
.
B
(
x
)
,
,
S
T
Lemmas
nat
wf
,
nat
plus
wf
,
nat
plus
inc
int
nzero
,
divide
wfa
,
div
nrel
wf
,
divide
wf
,
div
fun
sat
div
nrel
origin
a:
, n:
. 
q:. (Div(a;n;q) & (a 
n) = q 
) a:, n:. q:. (Div(a;n;q) & (a n) = q ) Tx:A. B(x)
x:A. B(x)
T